{
 "cells": [
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "# 假设\n",
    "\n",
    "一个实现逻辑谓词和假设系统的模块。\n",
    "\n",
    "## 断言\n",
    "\n",
    "### 类 class sympy.assumptions.assume.Predicate (*args, **kwargs)\n",
    "\n",
    "数学谓词的基类。它还充当未定义谓词对象的构造函数。\n",
    "\n",
    "#### 解释\n",
    "\n",
    "Predicate 是返回布尔值[1]的函数。\n",
    "\n",
    "谓词函数是对象，是谓词类的实例。将谓词应用于参数时，将返回 `AppliedPredicate` 实例。这仅仅是包装了论点，并且保持未计算状态。为了获得应用谓词的真值，使用函数 `ask`。\n",
    "\n",
    "谓词的求值是通过多个分派来完成的。您可以将新的处理程序注册到谓词中以支持新的类型。\n",
    "\n",
    "SymPy 中的每个谓词都可以通过 `Q`.的属性访问。例如，`Q.even` 返回一个谓词，用于检查参数是否为偶数。\n",
    "\n",
    "为了定义一个可以计算的谓词，您必须对这个类进行子类化，创建它的实例，并将它注册到 `Q`。然后，根据参数类型分派处理程序。\n",
    "\n",
    "如果您使用这个类直接构造谓词，您将得到无法调度的 `UndefinedPredicate` 。这在构建不需要求值的布尔表达式时非常有用。\n",
    "\n",
    "#### 例子\n",
    "\n",
    "应用和计算布尔值:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 1,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 1,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy import Q, ask\n",
    "ask(Q.prime(7))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "您可以通过子类化和分派来定义一个新的谓词。在这里，我们定义了一个名为`性感素数`的谓词[2]作为一个例子。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 2,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 2,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy import Predicate, Integer\n",
    "\n",
    "class SexyPrimePredicate(Predicate):\n",
    "    name = \"sexyprime\"\n",
    "\n",
    "Q.sexyprime = SexyPrimePredicate()\n",
    "@Q.sexyprime.register(Integer, Integer)\n",
    "def _(int1, int2, assumptions):\n",
    "    args = sorted([int1, int2])\n",
    "    if not all(ask(Q.prime(a), assumptions) for a in args):\n",
    "        return False\n",
    "    return args[1] - args[0] == 6\n",
    "ask(Q.sexyprime(5, 11))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "直接构造返回 UndefinedPredicate，它可以应用但不能被分派。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 3,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "sympy.assumptions.assume.UndefinedPredicate"
      ]
     },
     "execution_count": 3,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy import Predicate, Integer\n",
    "Q.P = Predicate(\"P\")\n",
    "type(Q.P)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 4,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle Q.P(1)$"
      ],
      "text/plain": [
       "Q.P(1)"
      ]
     },
     "execution_count": 4,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "Q.P(1)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 5,
   "metadata": {},
   "outputs": [
    {
     "ename": "TypeError",
     "evalue": "<class 'sympy.assumptions.assume.PredicateMeta'> cannot be dispatched.",
     "output_type": "error",
     "traceback": [
      "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[0;31mTypeError\u001b[0m                                 Traceback (most recent call last)",
      "\u001b[0;32m<ipython-input-5-9cc711c81391>\u001b[0m in \u001b[0;36m<module>\u001b[0;34m\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mQ\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mP\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mregister\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mInteger\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;32mlambda\u001b[0m \u001b[0mexpr\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0massump\u001b[0m\u001b[0;34m:\u001b[0m \u001b[0;32mTrue\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
      "\u001b[0;32m/opt/anaconda3/lib/python3.8/site-packages/sympy/assumptions/assume.py\u001b[0m in \u001b[0;36mregister\u001b[0;34m(cls, *types, **kwargs)\u001b[0m\n\u001b[1;32m    331\u001b[0m         \"\"\"\n\u001b[1;32m    332\u001b[0m         \u001b[0;32mif\u001b[0m \u001b[0mcls\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mhandler\u001b[0m \u001b[0;32mis\u001b[0m \u001b[0;32mNone\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 333\u001b[0;31m             \u001b[0;32mraise\u001b[0m \u001b[0mTypeError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"%s cannot be dispatched.\"\u001b[0m \u001b[0;34m%\u001b[0m \u001b[0mtype\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mcls\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m    334\u001b[0m         \u001b[0;32mreturn\u001b[0m \u001b[0mcls\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mhandler\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mregister\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m*\u001b[0m\u001b[0mtypes\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0;34m**\u001b[0m\u001b[0mkwargs\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    335\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;31mTypeError\u001b[0m: <class 'sympy.assumptions.assume.PredicateMeta'> cannot be dispatched."
     ]
    }
   ],
   "source": [
    "Q.P.register(Integer)(lambda expr, assump: True)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "### 参考资料\n",
    "\n",
    "[R3] https://en.wikipedia.org/wiki/Predicate_(mathematical_logic)\n",
    "\n",
    "[R4] https://en.wikipedia.org/wiki/Sexy_prime\n",
    "\n",
    "#### eval(args, assumptions=True)\n",
    "\n",
    "在给定的假设下评估自身(* args)。\n",
    "\n",
    "这只使用直接解析方法，而不使用逻辑推理。\n",
    "\n",
    "#### handler = <dispatched AskPredicateHandler>\n",
    "\n",
    "#### 类 classmethod register(*types, **kwargs)\n",
    "\n",
    "向处理程序注册签名。\n",
    "\n",
    "#### 类 classmethod register_many(*types, **kwargs)\n",
    "\n",
    "向同一处理程序注册多个签名。\n",
    "\n",
    "#### 类 class sympy.assumptions.assume.AppliedPredicate(predicate, *args)\n",
    "\n",
    "由于将 Predicate 应用于参数而产生的表达式类。AppliedPredicate 仅仅包装它的参数并保持未计算状态。要评估它，请使用 `ask()`函数。\n",
    "\n",
    "#### 示例"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 6,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle Q.integer(1)$"
      ],
      "text/plain": [
       "Q.integer(1)"
      ]
     },
     "execution_count": 6,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy import Q, ask\n",
    "Q.integer(1)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "`function` 属性返回谓词，`arguments` 属性返回参数的元组。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 8,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "<class 'sympy.assumptions.assume.AppliedPredicate'>\n",
      "Q.integer\n",
      "(1,)\n"
     ]
    }
   ],
   "source": [
    "print(type(Q.integer(1)))\n",
    "print(Q.integer(1).function)\n",
    "print(Q.integer(1).arguments)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "应用谓词可以计算到一个布尔值 `ask`:"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 9,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/plain": [
       "True"
      ]
     },
     "execution_count": 9,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "ask(Q.integer(1))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### 属性 arg\n",
    "\n",
    "返回该假设使用的表达式。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 10,
   "metadata": {},
   "outputs": [
    {
     "data": {
      "text/latex": [
       "$\\displaystyle x + 1$"
      ],
      "text/plain": [
       "x + 1"
      ]
     },
     "execution_count": 10,
     "metadata": {},
     "output_type": "execute_result"
    }
   ],
   "source": [
    "from sympy import Q, Symbol\n",
    "x = Symbol('x')\n",
    "a = Q.integer(x + 1)\n",
    "a.arg"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### 属性 arguments\n",
    "\n",
    "返回应用于谓词的参数。\n",
    "\n",
    "#### 属性 function\n",
    "\n",
    "返回谓词。\n",
    "\n",
    "## 询问\n",
    "\n",
    "查询用于询问有关表达式的信息。主要的方法是 `ask()` :\n",
    "\n",
    "### 函数 sympy.assumptions.ask.ask(proposition, assumptions=True, context={}{})\n",
    "\n",
    "用假设评价命题的函数。\n",
    "\n",
    "#### 参数 proposition : Any\n",
    "\n",
    "命题: 任何布尔表达式。\n",
    "\n",
    "命题将被求值为布尔值。如果不是 `AppliedPredicate`，它将被 `Q.is_true` 包装。\n",
    "\n",
    "#### 参数 assumptions : Any boolean expression, optional. \n",
    "\n",
    "假设: 任何布尔表达式，可选。\n",
    "\n",
    "局部假设来评估命题。\n",
    "\n",
    "#### 参数 context : AssumptionsContext, optional.\n",
    "\n",
    "上下文: AssumptionsContext，可选。\n",
    "\n",
    "默认假设来评估命题。默认情况下，是`sympy.assumptions.global_assumptions`变量。\n",
    "\n",
    "#### 返回 True, False, or None\n",
    "\n",
    "真，假，或空\n",
    "\n",
    "#### 抛出 Raises \n",
    "\n",
    "TypeError : proposition or assumptions is not valid logical expression.\n",
    "\n",
    "类型错误: 命题或假设不是有效的逻辑表达式。\n",
    "\n",
    "ValueError : assumptions are inconsistent.\n",
    "\n",
    "值错误: 假设是不一致的。\n",
    "\n",
    "#### 解释\n",
    "\n",
    "如果可以确定真值，则此函数将命题计算为 True 或 False。如果没有，则返回 None。\n",
    "\n",
    "它应该从 `refine()`中辨别出来，`refine()`应用于一个命题时，将参数简化为符号布尔值，而不是 Python 内置的 `True`、 `False` 或 `None`。\n",
    "\n",
    "#### 语法\n",
    "\n",
    "ask(proposition) \n",
    "请求(提议)\n",
    "\n",
    "在全局假设语境中评价命题。\n",
    "\n",
    "ask(proposition, assumptions) 询问(命题、假设)\n",
    "\n",
    "在全局假设上下文中评价假设的命题。\n",
    "\n",
    "#### 例子"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 11,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "False\n",
      "True\n",
      "False\n"
     ]
    }
   ],
   "source": [
    "from sympy import ask, Q, pi\n",
    "from sympy.abc import x, y\n",
    "print(ask(Q.rational(pi)))\n",
    "print(ask(Q.even(x*y), Q.even(x) & Q.integer(y)))\n",
    "print(ask(Q.prime(4*x), Q.integer(x)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "如果不能确定真值，则不返回真值。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 12,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "None\n"
     ]
    }
   ],
   "source": [
    "print(ask(Q.odd(3*x))) # cannot determine unless we know x"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "如果假设不一致，则引发 ValueError。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 13,
   "metadata": {},
   "outputs": [
    {
     "ename": "ValueError",
     "evalue": "inconsistent assumptions Q.odd(x) & Q.even(x)",
     "output_type": "error",
     "traceback": [
      "\u001b[0;31m---------------------------------------------------------------------------\u001b[0m",
      "\u001b[0;31mValueError\u001b[0m                                Traceback (most recent call last)",
      "\u001b[0;32m<ipython-input-13-e3bb329dace3>\u001b[0m in \u001b[0;36m<module>\u001b[0;34m\u001b[0m\n\u001b[0;32m----> 1\u001b[0;31m \u001b[0mask\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mQ\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0minteger\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mx\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m,\u001b[0m \u001b[0mQ\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0meven\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mx\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;34m&\u001b[0m \u001b[0mQ\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0modd\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0mx\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m",
      "\u001b[0;32m/opt/anaconda3/lib/python3.8/site-packages/sympy/assumptions/ask.py\u001b[0m in \u001b[0;36mask\u001b[0;34m(proposition, assumptions, context)\u001b[0m\n\u001b[1;32m    424\u001b[0m     \u001b[0;31m# check the satisfiability of given assumptions\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    425\u001b[0m     \u001b[0;32mif\u001b[0m \u001b[0mlocal_facts\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mclauses\u001b[0m \u001b[0;32mand\u001b[0m \u001b[0msatisfiable\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0menc_cnf\u001b[0m\u001b[0;34m)\u001b[0m \u001b[0;32mis\u001b[0m \u001b[0;32mFalse\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0;32m--> 426\u001b[0;31m         \u001b[0;32mraise\u001b[0m \u001b[0mValueError\u001b[0m\u001b[0;34m(\u001b[0m\u001b[0;34m\"inconsistent assumptions %s\"\u001b[0m \u001b[0;34m%\u001b[0m \u001b[0massumptions\u001b[0m\u001b[0;34m)\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n\u001b[0m\u001b[1;32m    427\u001b[0m \u001b[0;34m\u001b[0m\u001b[0m\n\u001b[1;32m    428\u001b[0m     \u001b[0;32mif\u001b[0m \u001b[0mlocal_facts\u001b[0m\u001b[0;34m.\u001b[0m\u001b[0mclauses\u001b[0m\u001b[0;34m:\u001b[0m\u001b[0;34m\u001b[0m\u001b[0;34m\u001b[0m\u001b[0m\n",
      "\u001b[0;31mValueError\u001b[0m: inconsistent assumptions Q.odd(x) & Q.even(x)"
     ]
    }
   ],
   "source": [
    "ask(Q.integer(x), Q.even(x) & Q.odd(x))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "#### 注释\n",
    "\n",
    "假设中的关系尚未实现，因此下面的结论不会给出有意义的结果。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 14,
   "metadata": {},
   "outputs": [],
   "source": [
    "ask(Q.positive(x), x > 0)"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "然而，这是一项正在进行的工作。\n",
    "\n",
    "#### 参见\n",
    "\n",
    "`sympy.assumptions.refine.refine`\n",
    "\n",
    "使用假设进行简化。如果真值不能确定，命题就不能简化为无。\n",
    "\n",
    "`ask` 可选的第二个参数应该是一个布尔表达式，涉及 `expr` 中对象的假设, 可用的值包含:\n",
    "\n",
    "- Q.integer(x)\n",
    "- Q.positive(x)\n",
    "- Q.integer(x) & Q.positive(x)\n",
    "- 等等\n",
    "\n",
    "`Q` 是一个包含已知谓词的对象。\n",
    "\n",
    "有关有效布尔表达式的完整列表，请参阅逻辑模块的文档。\n",
    "\n",
    "还可以定义一个上下文，这样就不必每次都传递该参数来执行 `ask()`函数。这是通过使用来自模块 `sympy.assumptions` 的假设上下文管理器来实现的。"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": 15,
   "metadata": {},
   "outputs": [
    {
     "name": "stdout",
     "output_type": "stream",
     "text": [
      "True\n"
     ]
    }
   ],
   "source": [
    "from sympy import *\n",
    "x = Symbol('x')\n",
    "y = Symbol('y')\n",
    "facts = Q.positive(x), Q.positive(y)\n",
    "with assuming(*facts):\n",
    "    print(ask(Q.positive(2*x + y)))"
   ]
  },
  {
   "cell_type": "markdown",
   "metadata": {},
   "source": [
    "## 内容\n",
    "\n",
    "Ask 询问\n",
    "Assume 假设\n",
    "Refine 精炼\n",
    "Predicates 谓词\n",
    "    Common 常见问题\n",
    "        Tautological 同义反复的\n",
    "        Commutative 交换性\n",
    "    Calculus 微积分\n",
    "        Finite 有限的\n",
    "        Infinite 无穷无尽\n",
    "    Matrix 矩阵\n",
    "        Symmetric 对称的\n",
    "        Invertible 可逆\n",
    "        Orthogonal 正交的\n",
    "        Unitary 单一制\n",
    "        Positive Definite 正定\n",
    "        Upper triangular 上三角形\n",
    "        Lower triangular 下三角形\n",
    "        Diagonal 对角线\n",
    "        Full rank 全级\n",
    "        Square 广场\n",
    "        Integer elements 整数元素\n",
    "        Real elements 真实元素\n",
    "        Complex elements 复杂元素\n",
    "        Singular 独一无二\n",
    "        Normal 正常\n",
    "        Triangular 三角形\n",
    "        Unit triangular 单位三角形\n",
    "    Number Theory 数论\n",
    "        Even 甚至\n",
    "        Odd 奇怪\n",
    "        Prime 质数\n",
    "        Composite 复合材料\n",
    "    Order 秩序\n",
    "        Positive 肯定\n",
    "        Negative 不行\n",
    "        Zero 零\n",
    "        Nonzero 非零\n",
    "        Nonpositive 非阳性\n",
    "        Nonnegative 非负数\n",
    "    Sets 集合\n",
    "        Integer 整数\n",
    "        Rational 理性\n",
    "        Irrational 非理性\n",
    "        Real 真的\n",
    "        Extended real 扩展实数\n",
    "        Hermitian 女名女子名\n",
    "        Complex 复杂\n",
    "        Imaginary 想象力\n",
    "        Antihermitian 安特尔米特的\n",
    "        Algebraic 代数\n",
    "        Transcendental 卓越的\n",
    "\n",
    "## 性能改进\n",
    "\n",
    "对于涉及符号系数的查询，将使用逻辑推理。提高可满足功能(`sympy.logic.inference.satisfiable`)的工作应该能够显著提高速度。\n",
    "\n",
    "一个问题中使用的逻辑推理可以用来加速进一步的查询，而目前的系统没有利用这一点。例如，可以实现真相维护系统( https://en.wikipedia.org/wiki/truth_maintenance_system )。\n",
    "\n",
    "## 其他\n",
    "\n",
    "可以在 sympy/assumption/tests/目录下的 test 形式中找到更多的示例"
   ]
  }
 ],
 "metadata": {
  "interpreter": {
   "hash": "40d3a090f54c6569ab1632332b64b2c03c39dcf918b08424e98f38b5ae0af88f"
  },
  "kernelspec": {
   "display_name": "Python 3.8.8 ('base')",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.8.8"
  },
  "orig_nbformat": 4
 },
 "nbformat": 4,
 "nbformat_minor": 2
}
